Mathematical constructivism
:This article is not about the application of the constructivist learning theory to mathematics. In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its existence, according to constructivists. See constructive proof. Constructivism is often confused with intuitionism, but in fact, intuitionism is only one kind of constructivism. Intuitionism maintains that the foundations of mathematics lie in the individual mathematician's intuition, thereby making mathematics into an intrinsically subjective activity. Constructivism does not, and is entirely consonant with an objective view of mathematics. Constructivist mathematics Constructivist mathematics uses constructivist logic, which is essentially a removal of the law of the excluded middle from classical logic. This is not to say that the law of the excluded middle is denied entirely; special cases of the law will be provable as theorems. It is just that the law is not assumed as an axiom. (The law of non-contradiction, on the other hand, is still valid.) For instance, in Heyting arithmetic, one can prove that for any proposition p'' which ''does not contain quantifiers, \forall x,y,z,... \in \mathbb{N} : p \vee \neg p is a theorem (where x'', ''y, z'' ... are the free variables in the proposition ''p). In this sense, propositions restricted to the finite are still regarded as being either true or false, as they are in classical mathematics, but this bivalence is not assumed to extend to those which talk about infinite collections. In fact, L.E.J. Brouwer, founder of the intuitionist school, viewed the law of the excluded middle as something which was abstracted from finite experience, and which was then applied by mathematicians to the infinite, without justification. For instance, Goldbach's conjecture is the assertion that every even number (greater than 2) is the sum of two prime numbers. It is possible to test for any particular even number whether or not it is the sum of two primes (for instance by exhaustive search), so it is fair to say of any one of them that it is either the sum of two primes, or it is not. And so far, every one thus tested has in fact been the sum of two primes. But there is no known proof that all of them are so, nor any known proof that not all of them are so. Thus to Brouwer, one cannot say "either Goldbach's conjecture is true, or it is not." And while the conjecture may one day be solved, the argument applies to similar unsolved problems; to Brouwer, the law of the excluded middle was tantamount to assuming that every mathematical problem has a solution. By doing away with the law of the excluded middle as an axiom, the remaining logical system has an existence property which classical logic does not: whenever \exists_{x\in X} P(x) is proven constructively, then in fact P(a) is proven constructively for (at least) one particular a\in X . Thus the proof of the existence of a mathematical object is tied to the possibility of its construction. Example from real analysis In classical real analysis, one way to define a real number is as a Cauchy sequence of rational numbers. In constructive mathematics, one way to construct a real number is as a function f that takes a positive integer n and outputs a rational f(n) , together with a function g that takes a positive integer n and outputs a positive integer g(n) such that : \forall n : \forall i,j \ge g(n) : |f(i) - f(j)| \le {1 \over n} so that as n increases, the values of f(n) get closer and closer together. We can use f and g together to compute as close a rational approximation as we like to the real number they represent. Under this definition, a simple representation of the real number ''e'' is: : f(n) = \sum_{i=0}^n {1 \over n!}, \; g(n) = n This definition corresponds to the classical definition using Cauchy sequences, except with a constructive twist: for a classical Cauchy sequence, it is required that, for any given distance, there exists (in a classical sense) a member in the sequence after which all members are closer together than that distance. In the constructive version, it is required that, for any given distance, it is possible to actually specify a point in the sequence where this happens (this required specification is often called the modulus of convergence). In fact, the standard constructive interpretation of the mathematical statement : \forall n : \exists m : \forall i,j \ge m: |f(i) - f(j)| \le {1 \over n} is precisely the existence of the function computing the modulus of convergence. Thus the difference between the two definitions of real numbers can be thought of as the difference in the interpretation of the statement "for all... there exists..." This then opens the question as to what sort of function from a countable set to a countable set, such as f'' and ''g above, can actually be constructed. Different versions of constructivism diverge on this point. Constructions can be defined as broadly as free choice sequences, which is the intuitionistic view, or as narrowly as algorithms (or more technically, the computable functions), or even left unspecified. If, for instance, the algorithmic view is taken, then the reals as constructed here are essentially what classically would be called the computable numbers. Cardinality To take the algorithmic interpretation above would seem at odds with classical notions of cardinality. By enumerating algorithms, we can show classically that the computable numbers are countable. And yet Cantor's diagonal argument shows that real numbers have higher cardinality. Furthermore the diagonal argument seems perfectly constructive. To identify the real numbers with the computable numbers would then be a contradiction. And in fact, Cantor's diagonal argument is constructive, in the sense that given a bijection between the real numbers and natural numbers, one constructs a real number which doesn't fit, and thereby proves a contradiction. We can indeed enumerate algorithms to construct a function T'' from the natural numbers onto the reals. But, to each algorithm, there may or may not correspond a real number, as the algorithm may fail to satisfy the constraints, or even be non-terminating (''T is a partial function), so this fails to produce the required bijection. Still, one might expect that since T'' is a partial function from the natural numbers onto the real numbers, that therefore the real numbers are ''no more than countable. And, since every natural number can be trivially represented as a real number, therefore the real numbers are no less than countable. They are, therefore exactly countable. However this reasoning is not constructive, as it still does not construct the required bijection. In fact the cardinality of sets fails to be totally ordered (see Cantor–Bernstein–Schroeder theorem). Axiom of choice A proof which requires the axiom of choice is regarded as non-constructive, as it asserts the existence of a certain choice function or set without it being possible to say what it is. The Goodman-Myhill theorem further showed that the law of the excluded middle could even be derived from the full axiom of choice. However restricted forms of the axiom of choice are sometimes employed. Attitude of mathematicians Traditionally, mathematicians have been suspicious, if not downright antagonistic, towards mathematical constructivism, largely because of the limitations that it poses for constructive analysis. These views were forcefully expressed by David Hilbert in 1928, when he wrote in Die Grundlagen der Mathematik, "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists" 1. (The law of excluded middle is not valid in constructivist logic.) Errett Bishop, in his 1967 work Foundations of Constructive Analysis, worked to dispel these fears by developing a great deal of traditional analysis in a constructive framework. Nevertheless, not every mathematician accepts that Bishop did so successfully, since his book is necessarily more complicated than a classical analysis text would be. In any case, most mathematicians see no need to restrict themselves to constructivist methods, even if this can be done. 1 Translation from the Stanford Encyclopedia of Philosophy, http://plato.stanford.edu/entries/mathematics-constructive/. Mathematicians who have contributed to constructivism * Errett Bishop * Paul Lorenzen * Leopold Kronecker (old constructivism) * L.E.J. Brouwer (intuitionism) * Arend Heyting (intuitionistic logic) Branches * Constructivist logic * Constructivist type theory * Constructivist analysis See also * Intuitionism * Intuitionistic type theory * Finitism * Game semantics * Constructive proof External links * Stanford Encyclopedia of Philosophy entry * Relationships between Constructive, Predicative, and Classical Systems of Analysis * Category:Epistemology de:Konstruktive Mathematik fr:Constructivisme (mathématiques) it:Costruttivismo matematico sv:Konstruktivism (matematik) tr:Oluşturmacı Matematik zh:数学结构主义